<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><link rel="stylesheet" type="text/css" href="style.css" /><script type="text/javascript" src="highlight.js"></script></head><body><pre><span class="hs-pragma">{-# LANGUAGE Trustworthy #-}</span><span>
</span><span id="line-2"></span><span class="hs-pragma">{-# LANGUAGE DataKinds #-}</span><span>
</span><span id="line-3"></span><span class="hs-pragma">{-# LANGUAGE KindSignatures #-}</span><span>
</span><span id="line-4"></span><span class="hs-pragma">{-# LANGUAGE TypeFamilies #-}</span><span>
</span><span id="line-5"></span><span class="hs-pragma">{-# LANGUAGE TypeOperators #-}</span><span>
</span><span id="line-6"></span><span class="hs-pragma">{-# LANGUAGE NoStarIsType #-}</span><span>
</span><span id="line-7"></span><span class="hs-pragma">{-# LANGUAGE FlexibleInstances #-}</span><span>
</span><span id="line-8"></span><span class="hs-pragma">{-# LANGUAGE FlexibleContexts #-}</span><span>
</span><span id="line-9"></span><span class="hs-pragma">{-# LANGUAGE ScopedTypeVariables #-}</span><span>
</span><span id="line-10"></span><span class="hs-pragma">{-# LANGUAGE ConstraintKinds #-}</span><span>
</span><span id="line-11"></span><span class="hs-pragma">{-# LANGUAGE ExistentialQuantification #-}</span><span>
</span><span id="line-12"></span><span class="hs-pragma">{-# LANGUAGE RankNTypes #-}</span><span>
</span><span id="line-13"></span><span class="hs-pragma">{-# LANGUAGE NoImplicitPrelude #-}</span><span>
</span><span id="line-14"></span><span class="hs-pragma">{-# LANGUAGE MagicHash #-}</span><span>
</span><span id="line-15"></span><span class="hs-pragma">{-# LANGUAGE PolyKinds #-}</span><span>
</span><span id="line-16"></span><span>
</span><span id="line-17"></span><span class="hs-comment">{-| This module is an internal GHC module.  It declares the constants used
in the implementation of type-level natural numbers.  The programmer interface
for working with type-level naturals should be defined in a separate library.

@since 4.10.0.0
-}</span><span>
</span><span id="line-23"></span><span>
</span><span id="line-24"></span><span class="hs-keyword">module</span><span> </span><span class="hs-identifier">GHC.TypeNats</span><span>
</span><span id="line-25"></span><span>  </span><span class="hs-special">(</span><span> </span><span class="annot"><span class="hs-comment">-- * Nat Kind</span></span><span>
</span><span id="line-26"></span><span>    </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier">Nat</span></a></span><span> </span><span class="hs-comment">-- declared in GHC.Types in package ghc-prim</span><span>
</span><span id="line-27"></span><span>
</span><span id="line-28"></span><span>    </span><span class="annot"><span class="hs-comment">-- * Linking type and value level</span></span><span>
</span><span id="line-29"></span><span>  </span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#KnownNat"><span class="hs-identifier">KnownNat</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#natVal"><span class="hs-identifier">natVal</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#natVal%27"><span class="hs-identifier">natVal'</span></a></span><span>
</span><span id="line-30"></span><span>  </span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#SomeNat"><span class="hs-identifier">SomeNat</span></a></span><span class="hs-special">(</span><span class="hs-glyph">..</span><span class="hs-special">)</span><span>
</span><span id="line-31"></span><span>  </span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#someNatVal"><span class="hs-identifier">someNatVal</span></a></span><span>
</span><span id="line-32"></span><span>  </span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#sameNat"><span class="hs-identifier">sameNat</span></a></span><span>
</span><span id="line-33"></span><span>
</span><span id="line-34"></span><span>    </span><span class="annot"><span class="hs-comment">-- * Functions on type literals</span></span><span>
</span><span id="line-35"></span><span>  </span><span class="hs-special">,</span><span> </span><span class="hs-keyword">type</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#%3C%3D"><span class="hs-operator">(&lt;=)</span></a></span><span class="hs-special">,</span><span> </span><span class="hs-keyword">type</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#%3C%3D%3F"><span class="hs-operator">(&lt;=?)</span></a></span><span class="hs-special">,</span><span> </span><span class="hs-keyword">type</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#%2B"><span class="hs-operator">(+)</span></a></span><span class="hs-special">,</span><span> </span><span class="hs-keyword">type</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#%2A"><span class="hs-operator">(*)</span></a></span><span class="hs-special">,</span><span> </span><span class="hs-keyword">type</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#%5E"><span class="hs-operator">(^)</span></a></span><span class="hs-special">,</span><span> </span><span class="hs-keyword">type</span><span> </span><span class="hs-special">(</span><span class="hs-glyph">-</span><span class="hs-special">)</span><span>
</span><span id="line-36"></span><span>  </span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#CmpNat"><span class="hs-identifier">CmpNat</span></a></span><span>
</span><span id="line-37"></span><span>  </span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#Div"><span class="hs-identifier">Div</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#Mod"><span class="hs-identifier">Mod</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#Log2"><span class="hs-identifier">Log2</span></a></span><span>
</span><span id="line-38"></span><span>
</span><span id="line-39"></span><span>  </span><span class="hs-special">)</span><span> </span><span class="hs-keyword">where</span><span>
</span><span id="line-40"></span><span>
</span><span id="line-41"></span><span class="hs-keyword">import</span><span> </span><span class="annot"><a href="GHC.Base.html"><span class="hs-identifier">GHC.Base</span></a></span><span class="hs-special">(</span><span class="annot"><a href="../../ghc-prim/src/GHC.Classes.html#Eq"><span class="hs-identifier">Eq</span></a></span><span class="hs-special">(</span><span class="hs-glyph">..</span><span class="hs-special">)</span><span class="hs-special">,</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Classes.html#Ord"><span class="hs-identifier">Ord</span></a></span><span class="hs-special">(</span><span class="hs-glyph">..</span><span class="hs-special">)</span><span class="hs-special">,</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Bool"><span class="hs-identifier">Bool</span></a></span><span class="hs-special">(</span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#True"><span class="hs-identifier">True</span></a></span><span class="hs-special">)</span><span class="hs-special">,</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Ordering"><span class="hs-identifier">Ordering</span></a></span><span class="hs-special">(</span><span class="hs-glyph">..</span><span class="hs-special">)</span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.Base.html#otherwise"><span class="hs-identifier">otherwise</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-42"></span><span class="hs-keyword">import</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#"><span class="hs-identifier">GHC.Types</span></a></span><span class="hs-special">(</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier">Nat</span></a></span><span> </span><span class="hs-special">)</span><span>
</span><span id="line-43"></span><span class="hs-keyword">import</span><span> </span><span class="annot"><a href="../../ghc-bignum/src/GHC.Num.Natural.html#"><span class="hs-identifier">GHC.Num.Natural</span></a></span><span class="hs-special">(</span><span class="annot"><a href="../../ghc-bignum/src/GHC.Num.Natural.html#Natural"><span class="hs-identifier">Natural</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-44"></span><span class="hs-keyword">import</span><span> </span><span class="annot"><a href="GHC.Show.html"><span class="hs-identifier">GHC.Show</span></a></span><span class="hs-special">(</span><span class="annot"><a href="GHC.Show.html#Show"><span class="hs-identifier">Show</span></a></span><span class="hs-special">(</span><span class="hs-glyph">..</span><span class="hs-special">)</span><span class="hs-special">)</span><span>
</span><span id="line-45"></span><span class="hs-keyword">import</span><span> </span><span class="annot"><a href="GHC.Read.html"><span class="hs-identifier">GHC.Read</span></a></span><span class="hs-special">(</span><span class="annot"><a href="GHC.Read.html#Read"><span class="hs-identifier">Read</span></a></span><span class="hs-special">(</span><span class="hs-glyph">..</span><span class="hs-special">)</span><span class="hs-special">)</span><span>
</span><span id="line-46"></span><span class="hs-keyword">import</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Prim.html#"><span class="hs-identifier">GHC.Prim</span></a></span><span class="hs-special">(</span><span class="annot"><a href="../../ghc-prim/src/GHC.Prim.html#magicDict"><span class="hs-identifier">magicDict</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Prim.html#Proxy%23"><span class="hs-identifier">Proxy#</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-47"></span><span class="hs-keyword">import</span><span> </span><span class="annot"><a href="Data.Maybe.html"><span class="hs-identifier">Data.Maybe</span></a></span><span class="hs-special">(</span><span class="annot"><a href="GHC.Maybe.html#Maybe"><span class="hs-identifier">Maybe</span></a></span><span class="hs-special">(</span><span class="hs-glyph">..</span><span class="hs-special">)</span><span class="hs-special">)</span><span>
</span><span id="line-48"></span><span class="hs-keyword">import</span><span> </span><span class="annot"><a href="Data.Proxy.html"><span class="hs-identifier">Data.Proxy</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="Data.Proxy.html#Proxy"><span class="hs-identifier">Proxy</span></a></span><span class="hs-special">(</span><span class="hs-glyph">..</span><span class="hs-special">)</span><span class="hs-special">)</span><span>
</span><span id="line-49"></span><span class="hs-keyword">import</span><span> </span><span class="annot"><a href="Data.Type.Equality.html"><span class="hs-identifier">Data.Type.Equality</span></a></span><span class="hs-special">(</span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator">(:~:)</span></a></span><span class="hs-special">(</span><span class="annot"><a href="Data.Type.Equality.html#Refl"><span class="hs-identifier">Refl</span></a></span><span class="hs-special">)</span><span class="hs-special">)</span><span>
</span><span id="line-50"></span><span class="hs-keyword">import</span><span> </span><span class="annot"><a href="Unsafe.Coerce.html"><span class="hs-identifier">Unsafe.Coerce</span></a></span><span class="hs-special">(</span><span class="annot"><a href="Unsafe.Coerce.html#unsafeCoerce"><span class="hs-identifier">unsafeCoerce</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-51"></span><span>
</span><span id="line-52"></span><span class="hs-comment">--------------------------------------------------------------------------------</span><span>
</span><span id="line-53"></span><span>
</span><span id="line-54"></span><span class="hs-comment">-- | This class gives the integer associated with a type-level natural.</span><span>
</span><span id="line-55"></span><span class="hs-comment">-- There are instances of the class for every concrete literal: 0, 1, 2, etc.</span><span>
</span><span id="line-56"></span><span class="hs-comment">--</span><span>
</span><span id="line-57"></span><span class="hs-comment">-- @since 4.7.0.0</span><span>
</span><span id="line-58"></span><span class="hs-keyword">class</span><span> </span><span id="KnownNat"><span class="annot"><a href="GHC.TypeNats.html#KnownNat"><span class="hs-identifier hs-var">KnownNat</span></a></span></span><span> </span><span class="hs-special">(</span><span id="local-6989586621679506021"><span class="annot"><a href="#local-6989586621679506021"><span class="hs-identifier hs-type">n</span></a></span></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier hs-type">Nat</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-keyword">where</span><span>
</span><span id="line-59"></span><span>  </span><span id="natSing"><span class="annot"><a href="GHC.TypeNats.html#natSing"><span class="hs-identifier hs-type">natSing</span></a></span></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#SNat"><span class="hs-identifier hs-type">SNat</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506021"><span class="hs-identifier hs-type">n</span></a></span><span>
</span><span id="line-60"></span><span>
</span><span id="line-61"></span><span class="hs-comment">-- | @since 4.10.0.0</span><span>
</span><span id="line-62"></span><span class="annot"><a href="GHC.TypeNats.html#natVal"><span class="hs-identifier hs-type">natVal</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="hs-keyword">forall</span><span> </span><span id="local-6989586621679506026"><span class="annot"><a href="#local-6989586621679506026"><span class="hs-identifier hs-type">n</span></a></span></span><span> </span><span id="local-6989586621679506025"><span class="annot"><a href="#local-6989586621679506025"><span class="hs-identifier hs-type">proxy</span></a></span></span><span class="hs-operator">.</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#KnownNat"><span class="hs-identifier hs-type">KnownNat</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506026"><span class="hs-identifier hs-type">n</span></a></span><span> </span><span class="hs-glyph">=&gt;</span><span> </span><span class="annot"><a href="#local-6989586621679506025"><span class="hs-identifier hs-type">proxy</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506026"><span class="hs-identifier hs-type">n</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="../../ghc-bignum/src/GHC.Num.Natural.html#Natural"><span class="hs-identifier hs-type">Natural</span></a></span><span>
</span><span id="line-63"></span><span id="natVal"><span class="annot"><span class="annottext">natVal :: forall (n :: Nat) (proxy :: Nat -&gt; Type).
KnownNat n =&gt;
proxy n -&gt; Natural
</span><a href="GHC.TypeNats.html#natVal"><span class="hs-identifier hs-var hs-var">natVal</span></a></span></span><span> </span><span class="annot"><span class="annottext">proxy n
</span><span class="hs-identifier">_</span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="hs-keyword">case</span><span> </span><span class="annot"><span class="annottext">SNat n
forall (n :: Nat). KnownNat n =&gt; SNat n
</span><a href="GHC.TypeNats.html#natSing"><span class="hs-identifier hs-var">natSing</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#SNat"><span class="hs-identifier hs-type">SNat</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506026"><span class="hs-identifier hs-type">n</span></a></span><span> </span><span class="hs-keyword">of</span><span>
</span><span id="line-64"></span><span>             </span><span class="annot"><a href="GHC.TypeNats.html#SNat"><span class="hs-identifier hs-type">SNat</span></a></span><span> </span><span id="local-6989586621679505953"><span class="annot"><span class="annottext">Natural
</span><a href="#local-6989586621679505953"><span class="hs-identifier hs-var">x</span></a></span></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="annottext">Natural
</span><a href="#local-6989586621679505953"><span class="hs-identifier hs-var">x</span></a></span><span>
</span><span id="line-65"></span><span>
</span><span id="line-66"></span><span class="hs-comment">-- | @since 4.10.0.0</span><span>
</span><span id="line-67"></span><span class="annot"><a href="GHC.TypeNats.html#natVal%27"><span class="hs-identifier hs-type">natVal'</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="hs-keyword">forall</span><span> </span><span id="local-6989586621679506020"><span class="annot"><a href="#local-6989586621679506020"><span class="hs-identifier hs-type">n</span></a></span></span><span class="hs-operator">.</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#KnownNat"><span class="hs-identifier hs-type">KnownNat</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506020"><span class="hs-identifier hs-type">n</span></a></span><span> </span><span class="hs-glyph">=&gt;</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Prim.html#Proxy%23"><span class="hs-identifier hs-type">Proxy#</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506020"><span class="hs-identifier hs-type">n</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="../../ghc-bignum/src/GHC.Num.Natural.html#Natural"><span class="hs-identifier hs-type">Natural</span></a></span><span>
</span><span id="line-68"></span><span id="natVal%27"><span class="annot"><span class="annottext">natVal' :: forall (n :: Nat). KnownNat n =&gt; Proxy# n -&gt; Natural
</span><a href="GHC.TypeNats.html#natVal%27"><span class="hs-identifier hs-var hs-var">natVal'</span></a></span></span><span> </span><span class="annot"><span class="annottext">Proxy# n
</span><span class="hs-identifier">_</span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="hs-keyword">case</span><span> </span><span class="annot"><span class="annottext">SNat n
forall (n :: Nat). KnownNat n =&gt; SNat n
</span><a href="GHC.TypeNats.html#natSing"><span class="hs-identifier hs-var">natSing</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#SNat"><span class="hs-identifier hs-type">SNat</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506020"><span class="hs-identifier hs-type">n</span></a></span><span> </span><span class="hs-keyword">of</span><span>
</span><span id="line-69"></span><span>             </span><span class="annot"><a href="GHC.TypeNats.html#SNat"><span class="hs-identifier hs-type">SNat</span></a></span><span> </span><span id="local-6989586621679505950"><span class="annot"><span class="annottext">Natural
</span><a href="#local-6989586621679505950"><span class="hs-identifier hs-var">x</span></a></span></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="annottext">Natural
</span><a href="#local-6989586621679505950"><span class="hs-identifier hs-var">x</span></a></span><span>
</span><span id="line-70"></span><span>
</span><span id="line-71"></span><span class="hs-comment">-- | This type represents unknown type-level natural numbers.</span><span>
</span><span id="line-72"></span><span class="hs-comment">--</span><span>
</span><span id="line-73"></span><span class="hs-comment">-- @since 4.10.0.0</span><span>
</span><span id="line-74"></span><span class="hs-keyword">data</span><span> </span><span id="SomeNat"><span class="annot"><a href="GHC.TypeNats.html#SomeNat"><span class="hs-identifier hs-var">SomeNat</span></a></span></span><span>    </span><span class="hs-glyph">=</span><span> </span><span class="hs-keyword">forall</span><span> </span><span id="local-6989586621679506015"><span class="annot"><a href="#local-6989586621679506015"><span class="hs-identifier hs-type">n</span></a></span></span><span class="hs-operator">.</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#KnownNat"><span class="hs-identifier hs-type">KnownNat</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506015"><span class="hs-identifier hs-type">n</span></a></span><span>    </span><span class="hs-glyph">=&gt;</span><span> </span><span id="SomeNat"><span class="annot"><a href="GHC.TypeNats.html#SomeNat"><span class="hs-identifier hs-var">SomeNat</span></a></span></span><span>    </span><span class="hs-special">(</span><span class="annot"><a href="Data.Proxy.html#Proxy"><span class="hs-identifier hs-type">Proxy</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506015"><span class="hs-identifier hs-type">n</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-75"></span><span>
</span><span id="line-76"></span><span class="hs-comment">-- | Convert an integer into an unknown type-level natural.</span><span>
</span><span id="line-77"></span><span class="hs-comment">--</span><span>
</span><span id="line-78"></span><span class="hs-comment">-- @since 4.10.0.0</span><span>
</span><span id="line-79"></span><span class="annot"><a href="GHC.TypeNats.html#someNatVal"><span class="hs-identifier hs-type">someNatVal</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-bignum/src/GHC.Num.Natural.html#Natural"><span class="hs-identifier hs-type">Natural</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#SomeNat"><span class="hs-identifier hs-type">SomeNat</span></a></span><span>
</span><span id="line-80"></span><span id="someNatVal"><span class="annot"><span class="annottext">someNatVal :: Natural -&gt; SomeNat
</span><a href="GHC.TypeNats.html#someNatVal"><span class="hs-identifier hs-var hs-var">someNatVal</span></a></span></span><span> </span><span id="local-6989586621679505948"><span class="annot"><span class="annottext">Natural
</span><a href="#local-6989586621679505948"><span class="hs-identifier hs-var">n</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">(KnownNat Any =&gt; Proxy Any -&gt; SomeNat)
-&gt; SNat Any -&gt; Proxy Any -&gt; SomeNat
forall (a :: Nat) b.
(KnownNat a =&gt; Proxy a -&gt; b) -&gt; SNat a -&gt; Proxy a -&gt; b
</span><a href="GHC.TypeNats.html#withSNat"><span class="hs-identifier hs-var">withSNat</span></a></span><span> </span><span class="annot"><span class="annottext">KnownNat Any =&gt; Proxy Any -&gt; SomeNat
forall (n :: Nat). KnownNat n =&gt; Proxy n -&gt; SomeNat
</span><a href="GHC.TypeNats.html#SomeNat"><span class="hs-identifier hs-var">SomeNat</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">Natural -&gt; SNat Any
forall (n :: Nat). Natural -&gt; SNat n
</span><a href="GHC.TypeNats.html#SNat"><span class="hs-identifier hs-var">SNat</span></a></span><span> </span><span class="annot"><span class="annottext">Natural
</span><a href="#local-6989586621679505948"><span class="hs-identifier hs-var">n</span></a></span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">Proxy Any
forall {k} (t :: k). Proxy t
</span><a href="Data.Proxy.html#Proxy"><span class="hs-identifier hs-var">Proxy</span></a></span><span>
</span><span id="line-81"></span><span class="hs-pragma">{-# NOINLINE</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#someNatVal"><span class="hs-pragma hs-type">someNatVal</span></a></span><span> </span><span class="hs-pragma">#-}</span><span> </span><span class="hs-comment">-- See Note [NOINLINE someNatVal]</span><span>
</span><span id="line-82"></span><span>
</span><span id="line-83"></span><span class="hs-comment">{- Note [NOINLINE someNatVal]

`someNatVal` converts a natural number to an existentially quantified
dictionary for `KnowNat` (aka `SomeNat`).  The existential quantification
is very important, as it captures the fact that we don't know the type
statically, although we do know that it exists.   Because this type is
fully opaque, we should never be able to prove that it matches anything else.
This is why coherence should still hold:  we can manufacture a `KnownNat k`
dictionary, but it can never be confused with a `KnownNat 33` dictionary,
because we should never be able to prove that `k ~ 33`.

But how to implement `someNatVal`?  We can't quite implement it &quot;honestly&quot;
because `SomeNat` needs to &quot;hide&quot; the type of the newly created dictionary,
but we don't know what the actual type is!  If `someNatVal` was built into
the language, then we could manufacture a new skolem constant,
which should behave correctly.

Since extra language constructors have additional maintenance costs,
we use a trick to implement `someNatVal` in the library.  The idea is that
instead of generating a &quot;fresh&quot; type for each use of `someNatVal`, we simply
use GHC's placeholder type `Any` (of kind `Nat`). So, the elaborated
version of the code is:

  someNatVal n = withSNat @T (SomeNat @T) (SNat @T n) (Proxy @T)
    where type T = Any Nat

After inlining and simplification, this ends up looking something like this:

  someNatVal n = SomeNat @T (KnownNat @T (SNat @T n)) (Proxy @T)
    where type T = Any Nat

`KnownNat` is the constructor for dictionaries for the class `KnownNat`.
See Note [magicDictId magic] in &quot;basicType/MkId.hs&quot; for details on how
we actually construct the dictionary.

Note that using `Any Nat` is not really correct, as multilple calls to
`someNatVal` would violate coherence:

  type T = Any Nat

  x = SomeNat @T (KnownNat @T (SNat @T 1)) (Proxy @T)
  y = SomeNat @T (KnownNat @T (SNat @T 2)) (Proxy @T)

Note that now the code has two dictionaries with the same type, `KnownNat Any`,
but they have different implementations, namely `SNat 1` and `SNat 2`.  This
is not good, as GHC assumes coherence, and it is free to interchange
dictionaries of the same type, but in this case this would produce an incorrect
result.   See #16586 for examples of this happening.

We can avoid this problem by making the definition of `someNatVal` opaque
and we do this by using a `NOINLINE` pragma.  This restores coherence, because
GHC can only inspect the result of `someNatVal` by pattern matching on the
existential, which would generate a new type.  This restores correctness,
at the cost of having a little more allocation for the `SomeNat` constructors.
-}</span><span>
</span><span id="line-138"></span><span>
</span><span id="line-139"></span><span>
</span><span id="line-140"></span><span>
</span><span id="line-141"></span><span class="hs-comment">-- | @since 4.7.0.0</span><span>
</span><span id="line-142"></span><span class="hs-keyword">instance</span><span> </span><span id="local-6989586621679505941"><span class="annot"><a href="../../ghc-prim/src/GHC.Classes.html#Eq"><span class="hs-identifier hs-type">Eq</span></a></span><span> </span><span class="annot"><a href="GHC.TypeNats.html#SomeNat"><span class="hs-identifier hs-type">SomeNat</span></a></span></span><span> </span><span class="hs-keyword">where</span><span>
</span><span id="line-143"></span><span>  </span><span class="annot"><a href="GHC.TypeNats.html#SomeNat"><span class="hs-identifier hs-type">SomeNat</span></a></span><span> </span><span id="local-6989586621679505938"><span class="annot"><span class="annottext">Proxy n
</span><a href="#local-6989586621679505938"><span class="hs-identifier hs-var">x</span></a></span></span><span> </span><span id="local-6989586621679505937"><span class="annot"><span class="annottext">== :: SomeNat -&gt; SomeNat -&gt; Bool
</span><a href="../../ghc-prim/src/GHC.Classes.html#%3D%3D"><span class="hs-operator hs-var hs-var hs-var hs-var">==</span></a></span></span><span> </span><span class="annot"><a href="GHC.TypeNats.html#SomeNat"><span class="hs-identifier hs-type">SomeNat</span></a></span><span> </span><span id="local-6989586621679505931"><span class="annot"><span class="annottext">Proxy n
</span><a href="#local-6989586621679505931"><span class="hs-identifier hs-var">y</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">Proxy n -&gt; Natural
forall (n :: Nat) (proxy :: Nat -&gt; Type).
KnownNat n =&gt;
proxy n -&gt; Natural
</span><a href="GHC.TypeNats.html#natVal"><span class="hs-identifier hs-var">natVal</span></a></span><span> </span><span class="annot"><span class="annottext">Proxy n
</span><a href="#local-6989586621679505938"><span class="hs-identifier hs-var">x</span></a></span><span> </span><span class="annot"><span class="annottext">Natural -&gt; Natural -&gt; Bool
forall a. Eq a =&gt; a -&gt; a -&gt; Bool
</span><a href="../../ghc-prim/src/GHC.Classes.html#%3D%3D"><span class="hs-operator hs-var">==</span></a></span><span> </span><span class="annot"><span class="annottext">Proxy n -&gt; Natural
forall (n :: Nat) (proxy :: Nat -&gt; Type).
KnownNat n =&gt;
proxy n -&gt; Natural
</span><a href="GHC.TypeNats.html#natVal"><span class="hs-identifier hs-var">natVal</span></a></span><span> </span><span class="annot"><span class="annottext">Proxy n
</span><a href="#local-6989586621679505931"><span class="hs-identifier hs-var">y</span></a></span><span>
</span><span id="line-144"></span><span>
</span><span id="line-145"></span><span class="hs-comment">-- | @since 4.7.0.0</span><span>
</span><span id="line-146"></span><span class="hs-keyword">instance</span><span> </span><span id="local-6989586621679505916"><span id="local-6989586621679505918"><span id="local-6989586621679505920"><span id="local-6989586621679505922"><span id="local-6989586621679505924"><span id="local-6989586621679505926"><span class="annot"><a href="../../ghc-prim/src/GHC.Classes.html#Ord"><span class="hs-identifier hs-type">Ord</span></a></span><span> </span><span class="annot"><a href="GHC.TypeNats.html#SomeNat"><span class="hs-identifier hs-type">SomeNat</span></a></span></span></span></span></span></span></span><span> </span><span class="hs-keyword">where</span><span>
</span><span id="line-147"></span><span>  </span><span id="local-6989586621679505914"><span class="annot"><span class="annottext">compare :: SomeNat -&gt; SomeNat -&gt; Ordering
</span><a href="../../ghc-prim/src/GHC.Classes.html#compare"><span class="hs-identifier hs-var hs-var hs-var hs-var">compare</span></a></span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.TypeNats.html#SomeNat"><span class="hs-identifier hs-type">SomeNat</span></a></span><span> </span><span id="local-6989586621679505911"><span class="annot"><span class="annottext">Proxy n
</span><a href="#local-6989586621679505911"><span class="hs-identifier hs-var">x</span></a></span></span><span class="hs-special">)</span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.TypeNats.html#SomeNat"><span class="hs-identifier hs-type">SomeNat</span></a></span><span> </span><span id="local-6989586621679505905"><span class="annot"><span class="annottext">Proxy n
</span><a href="#local-6989586621679505905"><span class="hs-identifier hs-var">y</span></a></span></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">Natural -&gt; Natural -&gt; Ordering
forall a. Ord a =&gt; a -&gt; a -&gt; Ordering
</span><a href="../../ghc-prim/src/GHC.Classes.html#compare"><span class="hs-identifier hs-var">compare</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">Proxy n -&gt; Natural
forall (n :: Nat) (proxy :: Nat -&gt; Type).
KnownNat n =&gt;
proxy n -&gt; Natural
</span><a href="GHC.TypeNats.html#natVal"><span class="hs-identifier hs-var">natVal</span></a></span><span> </span><span class="annot"><span class="annottext">Proxy n
</span><a href="#local-6989586621679505911"><span class="hs-identifier hs-var">x</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">Proxy n -&gt; Natural
forall (n :: Nat) (proxy :: Nat -&gt; Type).
KnownNat n =&gt;
proxy n -&gt; Natural
</span><a href="GHC.TypeNats.html#natVal"><span class="hs-identifier hs-var">natVal</span></a></span><span> </span><span class="annot"><span class="annottext">Proxy n
</span><a href="#local-6989586621679505905"><span class="hs-identifier hs-var">y</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-148"></span><span>
</span><span id="line-149"></span><span class="hs-comment">-- | @since 4.7.0.0</span><span>
</span><span id="line-150"></span><span class="hs-keyword">instance</span><span> </span><span id="local-6989586621679505900"><span id="local-6989586621679505902"><span class="annot"><a href="GHC.Show.html#Show"><span class="hs-identifier hs-type">Show</span></a></span><span> </span><span class="annot"><a href="GHC.TypeNats.html#SomeNat"><span class="hs-identifier hs-type">SomeNat</span></a></span></span></span><span> </span><span class="hs-keyword">where</span><span>
</span><span id="line-151"></span><span>  </span><span id="local-6989586621679505898"><span class="annot"><span class="annottext">showsPrec :: Int -&gt; SomeNat -&gt; ShowS
</span><a href="GHC.Show.html#showsPrec"><span class="hs-identifier hs-var hs-var hs-var hs-var">showsPrec</span></a></span></span><span> </span><span id="local-6989586621679505896"><span class="annot"><span class="annottext">Int
</span><a href="#local-6989586621679505896"><span class="hs-identifier hs-var">p</span></a></span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.TypeNats.html#SomeNat"><span class="hs-identifier hs-type">SomeNat</span></a></span><span> </span><span id="local-6989586621679505891"><span class="annot"><span class="annottext">Proxy n
</span><a href="#local-6989586621679505891"><span class="hs-identifier hs-var">x</span></a></span></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">Int -&gt; Natural -&gt; ShowS
forall a. Show a =&gt; Int -&gt; a -&gt; ShowS
</span><a href="GHC.Show.html#showsPrec"><span class="hs-identifier hs-var">showsPrec</span></a></span><span> </span><span class="annot"><span class="annottext">Int
</span><a href="#local-6989586621679505896"><span class="hs-identifier hs-var">p</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">Proxy n -&gt; Natural
forall (n :: Nat) (proxy :: Nat -&gt; Type).
KnownNat n =&gt;
proxy n -&gt; Natural
</span><a href="GHC.TypeNats.html#natVal"><span class="hs-identifier hs-var">natVal</span></a></span><span> </span><span class="annot"><span class="annottext">Proxy n
</span><a href="#local-6989586621679505891"><span class="hs-identifier hs-var">x</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-152"></span><span>
</span><span id="line-153"></span><span class="hs-comment">-- | @since 4.7.0.0</span><span>
</span><span id="line-154"></span><span class="hs-keyword">instance</span><span> </span><span id="local-6989586621679505884"><span id="local-6989586621679505886"><span id="local-6989586621679505888"><span class="annot"><a href="GHC.Read.html#Read"><span class="hs-identifier hs-type">Read</span></a></span><span> </span><span class="annot"><a href="GHC.TypeNats.html#SomeNat"><span class="hs-identifier hs-type">SomeNat</span></a></span></span></span></span><span> </span><span class="hs-keyword">where</span><span>
</span><span id="line-155"></span><span>  </span><span id="local-6989586621679505878"><span class="annot"><span class="annottext">readsPrec :: Int -&gt; ReadS SomeNat
</span><a href="GHC.Read.html#readsPrec"><span class="hs-identifier hs-var hs-var hs-var hs-var">readsPrec</span></a></span></span><span> </span><span id="local-6989586621679505876"><span class="annot"><span class="annottext">Int
</span><a href="#local-6989586621679505876"><span class="hs-identifier hs-var">p</span></a></span></span><span> </span><span id="local-6989586621679505875"><span class="annot"><span class="annottext">String
</span><a href="#local-6989586621679505875"><span class="hs-identifier hs-var">xs</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="hs-keyword">do</span><span> </span><span class="hs-special">(</span><span id="local-6989586621679505874"><span class="annot"><span class="annottext">Natural
</span><a href="#local-6989586621679505874"><span class="hs-identifier hs-var">a</span></a></span></span><span class="hs-special">,</span><span id="local-6989586621679505873"><span class="annot"><span class="annottext">String
</span><a href="#local-6989586621679505873"><span class="hs-identifier hs-var">ys</span></a></span></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">&lt;-</span><span> </span><span class="annot"><span class="annottext">Int -&gt; ReadS Natural
forall a. Read a =&gt; Int -&gt; ReadS a
</span><a href="GHC.Read.html#readsPrec"><span class="hs-identifier hs-var">readsPrec</span></a></span><span> </span><span class="annot"><span class="annottext">Int
</span><a href="#local-6989586621679505876"><span class="hs-identifier hs-var">p</span></a></span><span> </span><span class="annot"><span class="annottext">String
</span><a href="#local-6989586621679505875"><span class="hs-identifier hs-var">xs</span></a></span><span>
</span><span id="line-156"></span><span>                      </span><span class="hs-special">[</span><span class="hs-special">(</span><span class="annot"><span class="annottext">Natural -&gt; SomeNat
</span><a href="GHC.TypeNats.html#someNatVal"><span class="hs-identifier hs-var">someNatVal</span></a></span><span> </span><span class="annot"><span class="annottext">Natural
</span><a href="#local-6989586621679505874"><span class="hs-identifier hs-var">a</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><span class="annottext">String
</span><a href="#local-6989586621679505873"><span class="hs-identifier hs-var">ys</span></a></span><span class="hs-special">)</span><span class="hs-special">]</span><span>
</span><span id="line-157"></span><span>
</span><span id="line-158"></span><span class="hs-comment">--------------------------------------------------------------------------------</span><span>
</span><span id="line-159"></span><span>
</span><span id="line-160"></span><span class="hs-keyword">infix</span><span>  </span><span class="hs-number">4</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#%3C%3D%3F"><span class="hs-operator hs-type">&lt;=?</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#%3C%3D"><span class="hs-operator hs-type">&lt;=</span></a></span><span>
</span><span id="line-161"></span><span class="hs-keyword">infixl</span><span> </span><span class="hs-number">6</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#%2B"><span class="hs-operator hs-type">+</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#-"><span class="hs-glyph hs-type">-</span></a></span><span>
</span><span id="line-162"></span><span class="hs-keyword">infixl</span><span> </span><span class="hs-number">7</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#%2A"><span class="hs-operator hs-type">*</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#Div"><span class="hs-operator hs-type">`Div`</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#Mod"><span class="hs-operator hs-type">`Mod`</span></a></span><span>
</span><span id="line-163"></span><span class="hs-keyword">infixr</span><span> </span><span class="hs-number">8</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#%5E"><span class="hs-operator hs-type">^</span></a></span><span>
</span><span id="line-164"></span><span>
</span><span id="line-165"></span><span class="hs-comment">-- | Comparison of type-level naturals, as a constraint.</span><span>
</span><span id="line-166"></span><span class="hs-comment">--</span><span>
</span><span id="line-167"></span><span class="hs-comment">-- @since 4.7.0.0</span><span>
</span><span id="line-168"></span><span class="hs-keyword">type</span><span> </span><span id="local-6989586621679505872"><span class="annot"><a href="#local-6989586621679505872"><span class="hs-identifier hs-type">x</span></a></span></span><span> </span><span id="%3C%3D"><span class="annot"><a href="GHC.TypeNats.html#%3C%3D"><span class="hs-operator hs-var">&lt;=</span></a></span></span><span> </span><span id="local-6989586621679505871"><span class="annot"><a href="#local-6989586621679505871"><span class="hs-identifier hs-type">y</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679505872"><span class="hs-identifier hs-type">x</span></a></span><span> </span><span class="annot"><a href="GHC.TypeNats.html#%3C%3D%3F"><span class="hs-operator hs-type">&lt;=?</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679505871"><span class="hs-identifier hs-type">y</span></a></span><span class="hs-special">)</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#~"><span class="hs-operator hs-type">~</span></a></span><span> </span><span class="hs-special">'</span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#True"><span class="hs-identifier hs-type">True</span></a></span><span>
</span><span id="line-169"></span><span>
</span><span id="line-170"></span><span class="hs-comment">-- | Comparison of type-level naturals, as a function.</span><span>
</span><span id="line-171"></span><span class="hs-comment">--</span><span>
</span><span id="line-172"></span><span class="hs-comment">-- @since 4.7.0.0</span><span>
</span><span id="line-173"></span><span class="hs-keyword">type</span><span> </span><span class="hs-keyword">family</span><span> </span><span id="CmpNat"><span class="annot"><a href="GHC.TypeNats.html#CmpNat"><span class="hs-identifier hs-var">CmpNat</span></a></span></span><span>    </span><span class="hs-special">(</span><span id="local-6989586621679505870"><span class="annot"><a href="#local-6989586621679505870"><span class="hs-identifier hs-type">m</span></a></span></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier hs-type">Nat</span></a></span><span class="hs-special">)</span><span>    </span><span class="hs-special">(</span><span id="local-6989586621679505869"><span class="annot"><a href="#local-6989586621679505869"><span class="hs-identifier hs-type">n</span></a></span></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier hs-type">Nat</span></a></span><span class="hs-special">)</span><span>    </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Ordering"><span class="hs-identifier hs-type">Ordering</span></a></span><span>
</span><span id="line-174"></span><span>
</span><span id="line-175"></span><span class="hs-comment">{- | Comparison of type-level naturals, as a function.
NOTE: The functionality for this function should be subsumed
by 'CmpNat', so this might go away in the future.
Please let us know, if you encounter discrepancies between the two. -}</span><span>
</span><span id="line-179"></span><span class="hs-keyword">type</span><span> </span><span class="hs-keyword">family</span><span> </span><span class="hs-special">(</span><span id="local-6989586621679505868"><span class="annot"><a href="#local-6989586621679505868"><span class="hs-identifier hs-type">m</span></a></span></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier hs-type">Nat</span></a></span><span class="hs-special">)</span><span> </span><span id="%3C%3D%3F"><span class="annot"><a href="GHC.TypeNats.html#%3C%3D%3F"><span class="hs-operator hs-var">&lt;=?</span></a></span></span><span> </span><span class="hs-special">(</span><span id="local-6989586621679505867"><span class="annot"><a href="#local-6989586621679505867"><span class="hs-identifier hs-type">n</span></a></span></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier hs-type">Nat</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Bool"><span class="hs-identifier hs-type">Bool</span></a></span><span>
</span><span id="line-180"></span><span>
</span><span id="line-181"></span><span class="hs-comment">-- | Addition of type-level naturals.</span><span>
</span><span id="line-182"></span><span class="hs-comment">--</span><span>
</span><span id="line-183"></span><span class="hs-comment">-- @since 4.7.0.0</span><span>
</span><span id="line-184"></span><span class="hs-keyword">type</span><span> </span><span class="hs-keyword">family</span><span> </span><span class="hs-special">(</span><span id="local-6989586621679505866"><span class="annot"><a href="#local-6989586621679505866"><span class="hs-identifier hs-type">m</span></a></span></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier hs-type">Nat</span></a></span><span class="hs-special">)</span><span> </span><span id="%2B"><span class="annot"><a href="GHC.TypeNats.html#%2B"><span class="hs-operator hs-var">+</span></a></span></span><span> </span><span class="hs-special">(</span><span id="local-6989586621679505865"><span class="annot"><a href="#local-6989586621679505865"><span class="hs-identifier hs-type">n</span></a></span></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier hs-type">Nat</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier hs-type">Nat</span></a></span><span>
</span><span id="line-185"></span><span>
</span><span id="line-186"></span><span class="hs-comment">-- | Multiplication of type-level naturals.</span><span>
</span><span id="line-187"></span><span class="hs-comment">--</span><span>
</span><span id="line-188"></span><span class="hs-comment">-- @since 4.7.0.0</span><span>
</span><span id="line-189"></span><span class="hs-keyword">type</span><span> </span><span class="hs-keyword">family</span><span> </span><span class="hs-special">(</span><span id="local-6989586621679505864"><span class="annot"><a href="#local-6989586621679505864"><span class="hs-identifier hs-type">m</span></a></span></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier hs-type">Nat</span></a></span><span class="hs-special">)</span><span> </span><span id="%2A"><span class="annot"><a href="GHC.TypeNats.html#%2A"><span class="hs-operator hs-var">*</span></a></span></span><span> </span><span class="hs-special">(</span><span id="local-6989586621679505863"><span class="annot"><a href="#local-6989586621679505863"><span class="hs-identifier hs-type">n</span></a></span></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier hs-type">Nat</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier hs-type">Nat</span></a></span><span>
</span><span id="line-190"></span><span>
</span><span id="line-191"></span><span class="hs-comment">-- | Exponentiation of type-level naturals.</span><span>
</span><span id="line-192"></span><span class="hs-comment">--</span><span>
</span><span id="line-193"></span><span class="hs-comment">-- @since 4.7.0.0</span><span>
</span><span id="line-194"></span><span class="hs-keyword">type</span><span> </span><span class="hs-keyword">family</span><span> </span><span class="hs-special">(</span><span id="local-6989586621679505862"><span class="annot"><a href="#local-6989586621679505862"><span class="hs-identifier hs-type">m</span></a></span></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier hs-type">Nat</span></a></span><span class="hs-special">)</span><span> </span><span id="%5E"><span class="annot"><a href="GHC.TypeNats.html#%5E"><span class="hs-operator hs-var">^</span></a></span></span><span> </span><span class="hs-special">(</span><span id="local-6989586621679505861"><span class="annot"><a href="#local-6989586621679505861"><span class="hs-identifier hs-type">n</span></a></span></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier hs-type">Nat</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier hs-type">Nat</span></a></span><span>
</span><span id="line-195"></span><span>
</span><span id="line-196"></span><span class="hs-comment">-- | Subtraction of type-level naturals.</span><span>
</span><span id="line-197"></span><span class="hs-comment">--</span><span>
</span><span id="line-198"></span><span class="hs-comment">-- @since 4.7.0.0</span><span>
</span><span id="line-199"></span><span class="hs-keyword">type</span><span> </span><span class="hs-keyword">family</span><span> </span><span class="hs-special">(</span><span id="local-6989586621679505860"><span class="annot"><a href="#local-6989586621679505860"><span class="hs-identifier hs-type">m</span></a></span></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier hs-type">Nat</span></a></span><span class="hs-special">)</span><span> </span><span id="-"><span class="annot"><a href="GHC.TypeNats.html#-"><span class="hs-glyph hs-var">-</span></a></span></span><span> </span><span class="hs-special">(</span><span id="local-6989586621679505859"><span class="annot"><a href="#local-6989586621679505859"><span class="hs-identifier hs-type">n</span></a></span></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier hs-type">Nat</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier hs-type">Nat</span></a></span><span>
</span><span id="line-200"></span><span>
</span><span id="line-201"></span><span class="hs-comment">-- | Division (round down) of natural numbers.</span><span>
</span><span id="line-202"></span><span class="hs-comment">-- @Div x 0@ is undefined (i.e., it cannot be reduced).</span><span>
</span><span id="line-203"></span><span class="hs-comment">--</span><span>
</span><span id="line-204"></span><span class="hs-comment">-- @since 4.11.0.0</span><span>
</span><span id="line-205"></span><span class="hs-keyword">type</span><span> </span><span class="hs-keyword">family</span><span> </span><span id="Div"><span class="annot"><a href="GHC.TypeNats.html#Div"><span class="hs-identifier hs-var">Div</span></a></span></span><span> </span><span class="hs-special">(</span><span id="local-6989586621679505858"><span class="annot"><a href="#local-6989586621679505858"><span class="hs-identifier hs-type">m</span></a></span></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier hs-type">Nat</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-special">(</span><span id="local-6989586621679505857"><span class="annot"><a href="#local-6989586621679505857"><span class="hs-identifier hs-type">n</span></a></span></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier hs-type">Nat</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier hs-type">Nat</span></a></span><span>
</span><span id="line-206"></span><span>
</span><span id="line-207"></span><span class="hs-comment">-- | Modulus of natural numbers.</span><span>
</span><span id="line-208"></span><span class="hs-comment">-- @Mod x 0@ is undefined (i.e., it cannot be reduced).</span><span>
</span><span id="line-209"></span><span class="hs-comment">--</span><span>
</span><span id="line-210"></span><span class="hs-comment">-- @since 4.11.0.0</span><span>
</span><span id="line-211"></span><span class="hs-keyword">type</span><span> </span><span class="hs-keyword">family</span><span> </span><span id="Mod"><span class="annot"><a href="GHC.TypeNats.html#Mod"><span class="hs-identifier hs-var">Mod</span></a></span></span><span> </span><span class="hs-special">(</span><span id="local-6989586621679505856"><span class="annot"><a href="#local-6989586621679505856"><span class="hs-identifier hs-type">m</span></a></span></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier hs-type">Nat</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-special">(</span><span id="local-6989586621679505855"><span class="annot"><a href="#local-6989586621679505855"><span class="hs-identifier hs-type">n</span></a></span></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier hs-type">Nat</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier hs-type">Nat</span></a></span><span>
</span><span id="line-212"></span><span>
</span><span id="line-213"></span><span class="hs-comment">-- | Log base 2 (round down) of natural numbers.</span><span>
</span><span id="line-214"></span><span class="hs-comment">-- @Log 0@ is undefined (i.e., it cannot be reduced).</span><span>
</span><span id="line-215"></span><span class="hs-comment">--</span><span>
</span><span id="line-216"></span><span class="hs-comment">-- @since 4.11.0.0</span><span>
</span><span id="line-217"></span><span class="hs-keyword">type</span><span> </span><span class="hs-keyword">family</span><span> </span><span id="Log2"><span class="annot"><a href="GHC.TypeNats.html#Log2"><span class="hs-identifier hs-var">Log2</span></a></span></span><span> </span><span class="hs-special">(</span><span id="local-6989586621679505854"><span class="annot"><a href="#local-6989586621679505854"><span class="hs-identifier hs-type">m</span></a></span></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier hs-type">Nat</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier hs-type">Nat</span></a></span><span>
</span><span id="line-218"></span><span>
</span><span id="line-219"></span><span class="hs-comment">--------------------------------------------------------------------------------</span><span>
</span><span id="line-220"></span><span>
</span><span id="line-221"></span><span class="hs-comment">-- | We either get evidence that this function was instantiated with the</span><span>
</span><span id="line-222"></span><span class="hs-comment">-- same type-level numbers, or 'Nothing'.</span><span>
</span><span id="line-223"></span><span class="hs-comment">--</span><span>
</span><span id="line-224"></span><span class="hs-comment">-- @since 4.7.0.0</span><span>
</span><span id="line-225"></span><span id="local-6989586621679505996"><span id="local-6989586621679505997"><span id="local-6989586621679505998"><span id="local-6989586621679505999"><span class="annot"><a href="GHC.TypeNats.html#sameNat"><span class="hs-identifier hs-type">sameNat</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.TypeNats.html#KnownNat"><span class="hs-identifier hs-type">KnownNat</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679505999"><span class="hs-identifier hs-type">a</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#KnownNat"><span class="hs-identifier hs-type">KnownNat</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679505998"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">=&gt;</span><span>
</span><span id="line-226"></span><span>           </span><span class="annot"><a href="#local-6989586621679505997"><span class="hs-identifier hs-type">proxy1</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679505999"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="#local-6989586621679505996"><span class="hs-identifier hs-type">proxy2</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679505998"><span class="hs-identifier hs-type">b</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="GHC.Maybe.html#Maybe"><span class="hs-identifier hs-type">Maybe</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679505999"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator hs-type">:~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679505998"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span></span></span></span></span><span>
</span><span id="line-227"></span><span id="sameNat"><span class="annot"><span class="annottext">sameNat :: forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -&gt; Type)
       (proxy2 :: Nat -&gt; Type).
(KnownNat a, KnownNat b) =&gt;
proxy1 a -&gt; proxy2 b -&gt; Maybe (a :~: b)
</span><a href="GHC.TypeNats.html#sameNat"><span class="hs-identifier hs-var hs-var">sameNat</span></a></span></span><span> </span><span id="local-6989586621679505848"><span class="annot"><span class="annottext">proxy1 a
</span><a href="#local-6989586621679505848"><span class="hs-identifier hs-var">x</span></a></span></span><span> </span><span id="local-6989586621679505847"><span class="annot"><span class="annottext">proxy2 b
</span><a href="#local-6989586621679505847"><span class="hs-identifier hs-var">y</span></a></span></span><span>
</span><span id="line-228"></span><span>  </span><span class="hs-glyph">|</span><span> </span><span class="annot"><span class="annottext">proxy1 a -&gt; Natural
forall (n :: Nat) (proxy :: Nat -&gt; Type).
KnownNat n =&gt;
proxy n -&gt; Natural
</span><a href="GHC.TypeNats.html#natVal"><span class="hs-identifier hs-var">natVal</span></a></span><span> </span><span class="annot"><span class="annottext">proxy1 a
</span><a href="#local-6989586621679505848"><span class="hs-identifier hs-var">x</span></a></span><span> </span><span class="annot"><span class="annottext">Natural -&gt; Natural -&gt; Bool
forall a. Eq a =&gt; a -&gt; a -&gt; Bool
</span><a href="../../ghc-prim/src/GHC.Classes.html#%3D%3D"><span class="hs-operator hs-var">==</span></a></span><span> </span><span class="annot"><span class="annottext">proxy2 b -&gt; Natural
forall (n :: Nat) (proxy :: Nat -&gt; Type).
KnownNat n =&gt;
proxy n -&gt; Natural
</span><a href="GHC.TypeNats.html#natVal"><span class="hs-identifier hs-var">natVal</span></a></span><span> </span><span class="annot"><span class="annottext">proxy2 b
</span><a href="#local-6989586621679505847"><span class="hs-identifier hs-var">y</span></a></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">(a :~: b) -&gt; Maybe (a :~: b)
forall a. a -&gt; Maybe a
</span><a href="GHC.Maybe.html#Just"><span class="hs-identifier hs-var">Just</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">(Any :~: Any) -&gt; a :~: b
forall a b. a -&gt; b
</span><a href="Unsafe.Coerce.html#unsafeCoerce"><span class="hs-identifier hs-var">unsafeCoerce</span></a></span><span> </span><span class="annot"><span class="annottext">Any :~: Any
forall {k} (a :: k). a :~: a
</span><a href="Data.Type.Equality.html#Refl"><span class="hs-identifier hs-var">Refl</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-229"></span><span>  </span><span class="hs-glyph">|</span><span> </span><span class="annot"><span class="annottext">Bool
</span><a href="GHC.Base.html#otherwise"><span class="hs-identifier hs-var">otherwise</span></a></span><span>            </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">Maybe (a :~: b)
forall a. Maybe a
</span><a href="GHC.Maybe.html#Nothing"><span class="hs-identifier hs-var">Nothing</span></a></span><span>
</span><span id="line-230"></span><span>
</span><span id="line-231"></span><span class="hs-comment">--------------------------------------------------------------------------------</span><span>
</span><span id="line-232"></span><span class="hs-comment">-- PRIVATE:</span><span>
</span><span id="line-233"></span><span>
</span><span id="line-234"></span><span class="hs-keyword">newtype</span><span> </span><span id="SNat"><span class="annot"><a href="GHC.TypeNats.html#SNat"><span class="hs-identifier hs-var">SNat</span></a></span></span><span>    </span><span class="hs-special">(</span><span id="local-6989586621679506014"><span class="annot"><a href="#local-6989586621679506014"><span class="hs-identifier hs-type">n</span></a></span></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Nat"><span class="hs-identifier hs-type">Nat</span></a></span><span class="hs-special">)</span><span>    </span><span class="hs-glyph">=</span><span> </span><span id="SNat"><span class="annot"><a href="GHC.TypeNats.html#SNat"><span class="hs-identifier hs-var">SNat</span></a></span></span><span>    </span><span class="annot"><a href="../../ghc-bignum/src/GHC.Num.Natural.html#Natural"><span class="hs-identifier hs-type">Natural</span></a></span><span>
</span><span id="line-235"></span><span>
</span><span id="line-236"></span><span class="hs-keyword">data</span><span> </span><span id="WrapN"><span class="annot"><a href="GHC.TypeNats.html#WrapN"><span class="hs-identifier hs-var">WrapN</span></a></span></span><span> </span><span id="local-6989586621679505982"><span class="annot"><a href="#local-6989586621679505982"><span class="hs-identifier hs-type">a</span></a></span></span><span> </span><span id="local-6989586621679505981"><span class="annot"><a href="#local-6989586621679505981"><span class="hs-identifier hs-type">b</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span id="WrapN"><span class="annot"><a href="GHC.TypeNats.html#WrapN"><span class="hs-identifier hs-var">WrapN</span></a></span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.TypeNats.html#KnownNat"><span class="hs-identifier hs-type">KnownNat</span></a></span><span>    </span><span class="annot"><a href="#local-6989586621679505982"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">=&gt;</span><span> </span><span class="annot"><a href="Data.Proxy.html#Proxy"><span class="hs-identifier hs-type">Proxy</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679505982"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="#local-6989586621679505981"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-237"></span><span>
</span><span id="line-238"></span><span class="hs-comment">-- See Note [magicDictId magic] in &quot;basicType/MkId.hs&quot;</span><span>
</span><span id="line-239"></span><span id="local-6989586621679506016"><span id="local-6989586621679506017"><span class="annot"><a href="GHC.TypeNats.html#withSNat"><span class="hs-identifier hs-type">withSNat</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.TypeNats.html#KnownNat"><span class="hs-identifier hs-type">KnownNat</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506017"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">=&gt;</span><span> </span><span class="annot"><a href="Data.Proxy.html#Proxy"><span class="hs-identifier hs-type">Proxy</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506017"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="#local-6989586621679506016"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-240"></span><span>         </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="GHC.TypeNats.html#SNat"><span class="hs-identifier hs-type">SNat</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506017"><span class="hs-identifier hs-type">a</span></a></span><span>      </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="Data.Proxy.html#Proxy"><span class="hs-identifier hs-type">Proxy</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506017"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="#local-6989586621679506016"><span class="hs-identifier hs-type">b</span></a></span></span></span><span>
</span><span id="line-241"></span><span id="withSNat"><span class="annot"><span class="annottext">withSNat :: forall (a :: Nat) b.
(KnownNat a =&gt; Proxy a -&gt; b) -&gt; SNat a -&gt; Proxy a -&gt; b
</span><a href="GHC.TypeNats.html#withSNat"><span class="hs-identifier hs-var hs-var">withSNat</span></a></span></span><span> </span><span id="local-6989586621679505845"><span class="annot"><span class="annottext">KnownNat a =&gt; Proxy a -&gt; b
</span><a href="#local-6989586621679505845"><span class="hs-identifier hs-var">f</span></a></span></span><span> </span><span id="local-6989586621679505844"><span class="annot"><span class="annottext">SNat a
</span><a href="#local-6989586621679505844"><span class="hs-identifier hs-var">x</span></a></span></span><span> </span><span id="local-6989586621679505843"><span class="annot"><span class="annottext">Proxy a
</span><a href="#local-6989586621679505843"><span class="hs-identifier hs-var">y</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">WrapN a b -&gt; SNat a -&gt; Proxy a -&gt; b
forall a. a
</span><a href="../../ghc-prim/src/GHC.Prim.html#magicDict"><span class="hs-identifier hs-var">magicDict</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">(KnownNat a =&gt; Proxy a -&gt; b) -&gt; WrapN a b
forall (a :: Nat) b. (KnownNat a =&gt; Proxy a -&gt; b) -&gt; WrapN a b
</span><a href="GHC.TypeNats.html#WrapN"><span class="hs-identifier hs-var">WrapN</span></a></span><span> </span><span class="annot"><span class="annottext">KnownNat a =&gt; Proxy a -&gt; b
</span><a href="#local-6989586621679505845"><span class="hs-identifier hs-var">f</span></a></span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">SNat a
</span><a href="#local-6989586621679505844"><span class="hs-identifier hs-var">x</span></a></span><span> </span><span class="annot"><span class="annottext">Proxy a
</span><a href="#local-6989586621679505843"><span class="hs-identifier hs-var">y</span></a></span><span>
</span><span id="line-242"></span></pre></body></html>